$\forall$$P$:(ES\{i\}$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$), $p$:es{-}real\{i:l\}(${\it es}$.$P$(${\it es}$)), ${\it es}$:ES\{i\}.
\\[0ex]Consistent(es{-}realizer($p$);${\it es}$) $\Rightarrow$ $P$(${\it es}$)